Show Navigation Frame |
![]() |
1 Process Parameters vs. Global Variables
Process Parameters (PP) and
Global Variables (GV)'s possible usages are shown in the following table.
The key difference is that Process Parameters can
not be updated during the evaluation. This is a price to pay for
efficient system exploration.
PP |
GV |
Examples | |
Used in event expressions |
Yes |
Yes |
var x = 0; P(i) = a.x -> P(i); P(i) = a.i -> P(i); |
Used as parameter for process |
Yes |
Yes |
var x = 0; P(i) = a -> P(x); P(i) = a -> P(i+2); |
LHS of event assignment |
No |
Yes |
var x = 0; P(i) = a{x=9;} -> P(i); P(i) = a{i=9;} -> P(i);
//(wrong) |
RHS of event assignment |
Yes |
Yes |
var x = 0; P(i) = a{x=x+1;} -> P(x); P(i) = a{x=i+1;} -> P(i); |
Channel output expression |
Yes |
Yes |
var x = 0; channel c 1; P(i) = c!x.x+1-> P(x); P(i) = c!i.i+1.x+i -> P(i); |
Channel input expression |
Yes |
No |
var x = 0; channel c 1; P(i) = c?x.x+1-> P(x);
//(wrong) P(i) = c?i.i+1 -> P(i); |
Channel input guard condition |
Yes |
Yes |
var x = 0; channel c 1; P(i) = c?[x+y+i>1]y -> P(i); P(i) = c?[y+i>1]y -> P(i);
|
Indexed Process Definition |
Yes |
No |
var x; Q = ||| i:{0..x} @ (a.i -> Skip);
//(wrong) P(m) = ||| i: {0..m} @ (a.i ->
Skip); |
Note: Channel input variables behave similarly to process parameters within their valid scope. Local variables behave similarly to global variables within their valid scope.
2 PAT Type System
The input languages of PAT are weak typing (a.k.a. loose typing) languages and therefore no typing information is required when declaring a variable. The process parameters and channel input variables can take in values with different types at different time. As long as there is no type mismatch (e.g., integer is used as an array or Boolean), the execution will proceed. Otherwise, invalid type casting exception will be thrown.
The advantage claimed of weak typing is that it requires less effort on the part of the programmer than strong typing, because the compiler or interpreter implicitly performs certain kinds of conversions. However, one claimed disadvantage is that weakly typed programming systems catch fewer errors at compile time and some of these might still remain after testing has been completed.
3 No-Synchronization on Data Operations
This is a common problem raised by many users that, for the following program, can the two processes P() and Q() synchronise on the event a? If not, then how to make them synchronise on 'a' and preserve the execution of statement block ({x++}) in an atomic fashion?
Answer:
No-Synchronization on Data Operations is a design decision to void data race. If two data operations can synchronize, the update of the same global variable can lead to data race. Therefore, PAT will give a warning that if there one data operation and an event with same in different processes running in parallel.
Back to the question, a intuitive solution is to put the event 'a' and increment statement in an atomic action as follows:
Then x will be updated right after a is engaged, and a will be synchronised.
The other possible solution could be:
4 Tips on using user defined data structures
Note that there is no difference between user defined types and normal variables (e.g. var x =1;). Only when the process parameter is used as user defined types, it is user's responsibility to make sure that the correct variable type is passed in since most of PAT modules don't have explicit types. See the example below.
#import "PAT.Lib.Set";
var<Set>
set1;
Q() =
P(set1);
P(i) = initialize{i.Add(1);}->
([i.GetSize() > 0] Skip);
Warning:
When the user defined data variable (declared as global variable) is used in conditions (if-then-else/guard/while-loop), the operation should be side-effect free. One example is the guard expression "i.GetSize() > 0" Otherwise the verification results may not be correct.
When user defined data structure is used as process parameter, if the parameter in the process updates the data structure, the verification/simulation maybe wrong and unexpected. For instance the following example, i is an object used in both branch of the choice operator, so the effect of executing add1 will stay even the actual branch selected is add2. In the simulator, you will find that after executing event add2, the value of set1 can become [1,2]. The root of this cause is the pointer problem. PAT will give warnings for such usage during parsing. It is user's responsibility to make sure the usage is correct.
#import "PAT.Lib.Set";
var<Set>
set1;
Q() =
P(set1);
P(i) = add1{i.Add(1);} -> Skip []
add2{i.Add(2);} -> Skip;
5 Tips on using string in LTL assertions.
PAT allows string in LTL assertions for complicated events like channel array events. However we don't do more refined parsing for the string. Therefore, we just compare the string with the event name. See the example below.
channel c[3] 1;
Sender(i) = c[i]!i -> Sender(i);
Receiver() = c[0]?x -> a.x -> Receiver() [] c[1]?x -> a.x ->
Receiver() [] c[2]?x -> a.x -> Receiver();
System() = (||| i:{0..2}@Sender(0)) ||| Receiver();
#assert System() |= []<> "c[1].value"; //Wrong
#assert System() |= []<> "c[1].1";
In the first assertion, value will not be instantiated to be 0, 1, or 2. So you have to specify the instance of the vaule clearly for the verification like the second assertion.
6 Operator Precedence
The operators at the top of the table bind more tightly than those lower
down.
Class | Operators | Description |
Expression | a[0] | Array Expression |
call (operation,arg1,..,argn) | Method Call | |
+expr, -expr | Unary Plus | |
!expr | Not | |
expr++, expr-- | Unary Addtion | |
*,/,% | Multiplication | |
+, - | Addition | |
<,>,<=,>= | Ordering | |
==, != | Equality | |
&, |, ^ | Bitwise | |
xor | Exclusive Or | |
&& | Conjunction | |
|| | Disjunction | |
Process Definition | chan!expr, chan?expr | Channel |
e->P | Event Prefix | |
case { cond1: P1 default: P } |
Case | |
atomic{P} | Atomic Sequence | |
if (cond) { P } else { Q } | Conditional Choice | |
ifa (cond) { P } else { Q } | Atomic Conditional Choices | |
ifb (cond) { P } | Blocking Conditional Choices | |
[cond]P | Guarded Process | |
P;Q | Sequential Composition | |
P\{e1,..,en} | Hiding | |
P interrupt Q | Interrupt | |
P[*]Q | External Choice | |
P<>Q | Internal Choice | |
P[]Q | General Choice | |
P||Q | Parallel Composition | |
P|||Q | Interleaving | |
P(x1, x2, ..., xn) = Exp; | Definition |